\documentclass[runningheads,a4paper,twocolumn]{llncs}

\usepackage{amssymb} \setcounter{tocdepth}{3}
\usepackage{graphicx}

\newcommand{\comment}[1]{}

\newcommand{\keywords}[1]{\par\addvspace\baselineskip
\noindent\keywordname\enspace\ignorespaces#1}

\begin{document}

\mainmatter  % start of an individual contribution

\title{Array Bound Verifier:\\A static analysis tool to check
the array bounds of C programs using the Z3 SAT Solver}

\titlerunning{Array Bound Verifier}

\author{Petey Aldous\\Balaji Soundrarajan} \authorrunning{Array
Bound Verifier}

\institute{University of Utah}

\toctitle{Array Bound Verifier} \tocauthor{Petey Aldous and
Balaji Soundrarajan} \maketitle

\section{Introduction}

Buffer overflow attacks have existed at least since 1988, when a
buffer overflow vulnerability in finger was exploited.
\cite{tour} Although researchers quickly discovered how the
attack worked and how to protect systems against them, buffer
overflow vulnerabilities continued to exist. It became apparent
that programming in C without introducing these vulnerabilities
is almost impossible for humans, so subsequent languages have
included dynamic array bounds checking. Such checks are
effective -- they entirely eliminate buffer overflows -- but
greatly diminish the speed of a program's execution. The result
is that programmers at present must choose between security and
speed.

In many cases, speed is not essential and programmers are
content to let their programs take whatever time is necessary to
execute. However, this is not always possible: programmers in
systems, video games, and other fields must coax every bit of
performance out of their programs. Because they need the
performance, they are forced to use C (or a variant) and then to
try to program securely.

The fact that every major operating system, no matter how
carefully it is designed, needs frequent security updates is
sufficient evidence that current techniques do not suffice to
secure C code.

In order to produce programs that are both performant and
secure, some technique must eliminate the performance bottleneck
in programs written in secure (with respect to buffer overflows)
languages or some technique must secure C programs.

Many languages have advanced techniques that grant them
significant speedups; for example, Java does JIT compilation.
Such optimizations are effective but do not address the latency
incurred by dynamic array bounds checks, nor does any of the
techniques provide enough speedup to compensate for the slowed
performance. The result is that performance-dependent fields use
C and its variants (most notably, C++), despite other languages'
optimizations.

If we assume that no optimization is possible that would
ameliorate or compensate for dynamic array bounds checks, the
only remaining solution is to secure C code. It is relatively
easy to do so by automatically adding checks to every array
reference, but such an approach duplicates what the other,
more secure, languages do -- and also duplicates the decrease
in performance that this approach incurs.

A static analysis of a C program could prove that it is secure
against buffer overflows. The fact that it is static means that
it would slow compilation but that it would not affect the
execution time of the program. Programmers could write as usual,
check their programs for vulnerabilities with a static analyzer,
modify their code to ensure security, and repeat the process
until the program is proven secure. This is a time-consuming
process, but it is certain to be preferable to releasing and
subsequently patching a program.

Being static, this analysis cannot be perfectly precise; the
halting problem makes it impossible. Instead, it must be a
conservative approximation that reports possible
vulnerabilities. It might fail to prove that a program is
secure, but if it reports that a program is secure, it is always
correct.

In this paper, we discuss a static analyzer that serves as a
proof of concept. It analyzes programs written in a small subset
of C. We claim that this subset is representative of the
language as a whole. We describe the functionality of the static
analyzer, show the results it gives, and discuss its soundness
and the certainty that it terminates.

\section{Discussion}

\subsection{Subset of C}

To simplify our proof of concept, we created a subset of C that
includes only a small subset of its features.

\subsubsection{Language Definition}

The included figures define our C subset and its
semantics. The symbols they use are defined as follows:

\begin{figure}
\caption{Grammar}
\label{grammar}
\begin{verbatim}
e :   <int>
    | e_1 op e_2
    | len(e)
    | var[e]
    | var

s :   e_1 = e_2;
    | if (e) goto l;
    | goto l;
    | int e_1 [ = e_2];

l_s:  s
    | l: s

op :  < | > | == | <= | >=

l:    var
\end{verbatim}
\end{figure}

{

\begin{itemize}
\item $X$ is the set of all variables. $x \in X$.

\item $E$ is the set of all expressions. $e \in E$.

\item $Z$ is the set of all integer values. $z \in Z$.

\item $\sigma$ is the store. $\sigma(x)$ retrieves a value from
the store. $\sigma \left[ x \leftarrow z \right]$ is the
store $\sigma$, but where the value of $x$ is $z$.

\item $P$ is the program. It acts as a function of line numbers,
returning the statement at the given number. For example,
$P(2)$ represents the statement at line 2. When given the
line number just beyond the last statement in the program,
$P$ returns the special symbol $end$.
\end{itemize}

First, we perform a superficial transformation on the program
to simplify its semantic definition: we number each line and
transform each label to a line number. It is an error to goto
a label that does not exist. Analogously, it is an error to go to a
line number that does not exist.

\clearpage
\begin{figure}
\caption{Semantics}
\label{semantics}
\addtolength{\parskip}{1em}
$\frac
{x \in Dom(\sigma) \; \;
\left< e, \, \sigma \right> \rightarrow \left< e', \, \sigma' \right>}
{\left< l \mathrm{:} \, x \, \mathrm{=} \, e, \, \sigma \right>
\rightarrow
\left< l \mathrm{:} \, x \, \mathrm{=} \, e', \, \sigma' \right>}
$

$\frac
{x \in Dom(\sigma)}
{\left< l \mathrm{:} \, x \, \mathrm{=} \, z, \, \sigma \right>
\rightarrow
\left< P(l+1), \,  \sigma \left[ x \leftarrow z \right] \right>}$

$\frac
{x \in Dom(\sigma) \; \;
\left< e, \, \sigma \right> \rightarrow \left< e', \, \sigma' \right>}
{\left< l \mathrm{: \, int} \; x \, \mathrm{=} \, e, \, \sigma \right>
\rightarrow
\left< l \mathrm{: \, int} \; x \, \mathrm{=} \, e', \, \sigma' \right>}
$

$\frac
{x \notin Dom(\sigma) \; \;
\left< e, \, \sigma \right> \rightarrow \left< e', \, \sigma' \right>}
{\left< l \mathrm{: \, int} \; x \mathrm{[} e \mathrm{]}, \, \sigma \right>
\rightarrow
\left< l \mathrm{: \, int} \; x \mathrm{[} e' \mathrm{]}, \, \sigma' \right>}$

$\frac
{x \notin Dom(\sigma) \; \;
\left< e, \, \sigma \right> \rightarrow \left< e', \, \sigma' \right>}
{\left< l \mathrm{: \, int} \; x \mathrm{[} e \mathrm{] \, = \{}
e_1, \, \dots \mathrm{\}}, \, \sigma \right>
\rightarrow
\left< l \mathrm{: \, int} \; x \mathrm{[} e' \mathrm{] \, = \{}
e_1, \, \dots \mathrm{\}}, \, \sigma' \right>}$

$\frac
{x \notin Dom(\sigma) \; \;
\left< e_1, \, \sigma \right> \rightarrow \left< e_1', \, \sigma' \right>}
{\left< l \mathrm{: \, int} \; x \mathrm{[} z \mathrm{] \, = \{}
z_1, \, \dots, e_1, \, \dots \mathrm{\}}, \, \sigma \right>
\rightarrow
\left< l \mathrm{: \, int} \; x \mathrm{[} z \mathrm{] \, = \{}
z_1, \, \dots, e_1', \, \dots \mathrm{\}}, \, \sigma' \right>}$

$\frac
{x \notin Dom(\sigma)}
{\left< l \mathrm{: \, int} \; x \mathrm{[} z \mathrm{] \, = \{}
z_1, \, \dots, \, z_z \mathrm{\}}, \, \sigma \right>
\rightarrow
\left< P(l+1), \, \sigma
\left[x \leftarrow undef \right]
\left[len(x) \leftarrow z \right]
\left[x[0] \leftarrow z_1 \right]
\left[x[1] \leftarrow z_2 \right]
\dots
\left[x[z-1] \leftarrow z_z \right]
\right>}$

$\frac
{x \notin Dom(\sigma)}
{\left< l \mathrm{: \, int} \; x \mathrm{[} z \mathrm{]}, \, \sigma \right>
\rightarrow
\left< P(l+1), \, \sigma
\left[x \leftarrow undef \right]
\left[len(x) \leftarrow z \right]
\left[x[0] \leftarrow undef \right]
\left[x[1] \leftarrow undef \right]
\dots
\left[x[z-1] \leftarrow undef \right]
\right>}$

$\frac
{x \notin Dom(\sigma)}
{\left< l\mathrm{: \, int} \; x \, \mathrm{=} \, z, \, \sigma \right>
\rightarrow
\left< P(l+1), \,  \sigma \left[ x \leftarrow z \right] \right>}$

$\frac{x \notin Dom(\sigma)}
{\left< l\mathrm{: \, int} \; x, \, \sigma \right>
\rightarrow
\left< P(l+1), \, \sigma \left[ x \leftarrow undef \right] \right>}$

$\frac{}
{\left< l_1 \mathrm{: \, goto} \; l_2, \, \sigma \right>
\rightarrow
\left< P(l_2), \, \sigma \right>}$

$\frac{\left< e, \, \sigma \right> \rightarrow \left< e' \sigma' \right>}
{\left<  l_1 \mathrm{: \, if \; (} e \mathrm{) \; goto} \; l_2, \, \sigma \right>
\rightarrow
\left< l_1\mathrm{: \, if \; (} e' \mathrm{) \; goto} \; l_2, \, \sigma' \right>}$

$\frac{}
{\left<  l_1\mathrm{: \, if \; (0) \; goto} \; l_2, \, \sigma \right>
\rightarrow
\left< P(l_1+1), \, \sigma \right>}$

$\frac{z \ne 0}
{\left< l_1\mathrm{: \, if \; (} z \mathrm{) \; goto} \; l_2, \, \sigma \right>
\rightarrow
\left< P(l_2), \, \sigma \right>}$

$\frac{}
{\left< end, \sigma \right> \rightarrow \mathrm{program \; terminates}}$

$\frac{z_1 > z_2}
{\left< z_1 \mathrm{>} z_2, \, \sigma \right>
\rightarrow
\left< 1, \, \sigma \right>}$

$\frac{\left< e_1, \, \sigma \right> \rightarrow \left< e_1', \, \sigma' \right>}
{\left< e_1 > e_2, \, \sigma \right> \rightarrow \left< e_1' > e_2, \, \sigma' \right>}$

$\frac{\left< e, \, \sigma \right> \rightarrow \left< e', \, \sigma' \right>}
{\left< z > e, \, \sigma \right> \rightarrow \left< z > e', \, \sigma' \right>}$

Other comparison operators are analogous.

$\frac{x \in Dom(\sigma)}
{\left< x, \, \sigma \right> \rightarrow \left< \sigma(x), \, \sigma \right>}$

$\frac{x \in Dom(\sigma) \; \;
\left< e, \, \sigma \right> \rightarrow \left< e', \, \sigma'\right>}
{\left<x[e], \, \sigma \right> \rightarrow \left< x[e'], \, \sigma' \right>}$

$\frac{x[z] \in Dom(\sigma)}
{\left<x[z], \, \sigma \right> \rightarrow \left< \sigma(x[z]), \, \sigma \right>}$

$\frac{len(x) \in Dom(\sigma)}
{\left< len(x), \, \sigma \right> \rightarrow \left< \sigma(len(x)), \, \sigma \right>}$

\end{figure}
}
\clearpage

\subsubsection{Description} The statements
included in the grammar are variable declarations, assignment
statements, goto statements, and conditional goto statements.
Notably absent are function definitions, function calls, control
structures, structs, unions, and the standard library.

The expressions are also limited. Variables have only one type
(\texttt{int}) and arrays are strictly one-dimensional. Binary
comparison operations are included. There is also a
\texttt{len()} primitive that gives the actual length of an
array.

\subsubsection{Analysis}

Although many language constructs are missing from our subset,
it is possible to duplicate the functionality of many of the
missing features with the included features. For example, a
conditional goto statement and a few goto statements can easily
duplicate an if statement exactly.

We do not claim to have analyzed C in its entirety; instead, we
claim to have shown that some programs in a C-like language can
be proven free of buffer overflow vulnerabilities. We claim that
this is an indication that a richer language, like C, might
conceivably be analyzed.

\subsection{Algorithm}

Our static analyzer performs an abstract interpretation of a C
program; that is, it interprets the program, but gives up some
precision in order to guarantee termination. Instead of storing
values, the abstract interpreter stores the sign (see below)
 of a value. It also stores a set of axioms that
describe what is known about a variable.

In order to calculate the sign of an expression, we use the
intuitive rules. The sign of a number is trivial to calculate.
Since other expressions are combinations of expressions, we
simply combine them; for example, the sum of two positive
expressions is positive (ignoring overflow). It may be
impossible to know the sign of an expression without
calculating its value; a sign in the abstract interpreter is
really a set of all possible signs. It may be certain that
an expression is nonnegative but not certain that it is
positive. It may also be impossible to determine anything
about the sign of an expression.

Whenever a variable is assigned, its sign must change and all
previously existing axioms
that include that variable must be eliminated. A new axiom
is added to reflect the change in the variable's value.

In contrast with a concrete interpreter, an abstract
interpreter traverses all possible paths. In our
subset, this means that it follows the obvious code path for
declaration statements, assignment statements, and goto
statements. In the case of a conditional goto, it follows
{\it both} paths that might be taken: the path through the
goto statement's target, where a concrete interpreter would jump when
the condition is true, and the path through the succeeding
statement, where a concrete interpreter would go whenever the
condition is false.

Of course, an abstract interpreter could have sufficient
information to prove or disprove the condition at any stage
of execution, making traversal of one path
unnecessary. In order to ensure that each branch can actually
execute, the abstract interpreter adds an axiom to each
branch of execution from a conditional goto.
On the true path (the path that continues at the
conditional goto statement's target), an axiom is added that asserts the
condition of the goto. This addition is sound because if the
condition is not true, the true branch is not executed.
Similarly, an axiom is added that asserts the logical inverse
of the goto statement's condition on the false path (the path that
continues on the statement that follows the conditional goto).
If the axioms are ever unsatisfiable, the path is not valid and
execution along this path in the abstract interpreter
terminates.

If the state of the interpreter (the combination of
control state, abstract store, and axioms) ever repeats itself,
we say that we have found a fixed point of the state space.
Left to itself, the abstract interpreter would loop
indefinitely, following the same path that it followed from the
repeated state, through some number of other states, and back
to the same repeated state. It will not discover any new
information as it repeats states, so terminating in this case
is sound. The fixed point calculation is not yet implemented,
so the interpreter loops indefinitely on almost any loop in a
C program.

The abstract interpreter also terminates whenever it reaches the
end of the program or if an array access cannot be proven to be
secure.

The algorithm terminates when all execution paths have
terminated or when one path reveals an array access that cannot
be proven to be secure. If no such path is found, the program
is secure with respect to array accesses.

\subsection{Implementation}

The first stages of our static analyzer are really
preprocessing. We lex and parse C code and then translate it
into an AST. The AST is then transposed from s-expressions into
an AST of Java objects. We then perform the static analysis as
described.

\subsubsection{Java AST} Our subset of C contains 4 types of
statements: declarations, assignments, conditional gotos, and
gotos. Each kind of statement is represented by a distinct Java
class. A preprocessing step is required to ensure that each Goto
object and each ConditionalGoto object refers to a valid
statement.

\subsubsection{Analysis}

After the preprocessing step, the analyzer starts traversing the
AST. The DeclarationStatement and AssignmentStatement store an
abstract value and, when it is available, the concrete value.
The concrete value is used to generate axioms during the
traversal. Either of these statements can have an array
reference as its L-value or its R-value. As soon as the analyzer
encounters an array reference, it extracts all the axioms
pertaining to the length of the array and the array referencing
expression, which could be an integer or a variable or another
array reference, and performs two satisfiability checks. The
first check ascertains that the referencing expression cannot
reference the array below the lower bound of the array (0) and
the second check ascertains that the referencing expression
cannot reference the array at or beyond the array
length. These two checks are sufficient to prove that the
reference is safe. The satisfiability check is performed
recursively if the referencing expression is again an array
reference. This satisfiability check is performed with the help
of Microsoft Research's Z3 SAT solver and these satisfiability
checks assure the safety of the array references within the C
program.

The analyzer also makes use of the SAT solver for the purpose of
branch pruning: it performs a satisfiability check on the axiom
set after each Conditional Goto (on each branch). If the axioms
are not satisfiable, the branch is pruned.
\comment{
When the analysis encounters a ConditionalGoto
statement, the analyzer takes both the true branch and the false
branch. In both of the branches, the corresponding condition is
added a set of axioms accumulated from other statements; on the
false branch, the condition is negated before its addition. A
satisfiability check is then performed on the resulting set of
axioms. If the axioms are not satisfiable, this means that the
current branch could not have been taken, so this branch of
execution terminates. When a branch of execution is terminated
in this manner, we say that it has been pruned.
}

\comment{
There are few other considerations that are vital for the proper
functioning of the analyzer. Whenever an l-value is assigned a
new value, all axioms with that l-value are removed because they
do not apply to the l-value's new value. }In order to
perform a fixed point calculation, our analyzer must record all
previously reached states.

\subsection{Termination}

The algorithm terminates because it has a finite state space and
because its fixed point calculation terminates whenever a state
is repeated.

The state space is the cross product of the program's statements,
an abstract store, and a set of axioms. The number of statements
is bounded by the size of the program, so it is clearly finite
for any finite program. The abstract store maps variables and
arrays (effectively, sequences of variables) to abstract values.
The number of variables is clearly bounded by the size of the
program, as is the number of arrays. Since arrays are allocated
statically, their size must also be bounded. This means that if
we represent an array $a$ of size $n$ as a sequence of
variables $a_0, a_1, \ldots, a_{n-1}$, the length of the
sequence is bounded because $n$ is bounded. Abstract values
are triples of booleans. Because it stores a bounded number of
constant-sized values, the abstract store must also have
finite size.

Bounding the size of the axiom set is slightly more difficult.
To do so, we must bound the size of axioms themselves. By doing
so, we can bound the size of the axiom set and then bound the
number of possible states of the axiom set.

An axiom relates two expressions. It includes an operator that
defines how the two elements are related. It can be stored as
a triple: an expression, an operator, and another expression.
Unlike the other values that are part of the state, axioms
can grow indefinitely as they refer to previously existing
axioms. For example, we might have an axiom $x = b$. Then, in
a loop, we might have $x = a + x$. If our abstract interpreter
is sufficiently advanced, it could create this axiom:
$x = a + b$. On the next loop, it could create
$x = a + a + b$. At each iteration, this axiom will continue
to grow. If the loop condition can't be proven to be false,
the abstract interpreter will repeat forever.

In order to prevent this unbounded growth,
we bound the size of axioms by restricting the size of the
expressions in them. If an expression is too large, its axiom
is removed from the analysis. This sacrifices precision but
not soundness (because axioms can prove soundness and their
absence cannot) and creates a finite bound on the size of
each axiom. Since axioms are bounded in size, they are also
bounded in number: only a finite number of discrete values
can exist if the values are bounded.

The state space, therefore, is bounded. It follows that with
a fixed point calculation, this analysis must terminate.

\subsection{Correctness}

Abstract interpretation is clearly similar to concrete
interpretation. It differs from concrete interpretation because
it traverses all possible execution paths and because it
discards information in some cases: truncating axioms is
necessary to guarantee termination but discards some precision.

This loss of precision is to be expected; we could not prove
termination if we had perfect precision because it would solve
the halting problem.

The information discarded is information that might have been
used to prove an array reference secure. It is clear that the
program might fail to prove that a program is safe when the
program is, in reality, safe. But because a lack of evidence
cannot contribute to a proof of safeness, this lack of precision
cannot create false negatives. In other words, our static
analyzer cannot report that all array references are safe if any
reference might be unsafe.

\section{Results}

\subsection{Examples}

The following figures show the results of the array bound verifier
for a few sample C programs.

\begin{figure}
\caption{Program 1 C Code}
\label{p1code}
\begin{verbatim}
     int x[3] = {1,2,3};
     int a = 2;
     int b;
     int c = 2;
     if (b<0) goto end;
     if (b>2) goto end;
     a = x[b];
end: c = 3;
\end{verbatim}
\end{figure}

In \ref{p1code}, the fixed point calculation has no effect;
it cannot ever reach the same control state twice, so it
never reaches a fixed point. However, it is informative to
demonstrate such a calculation.

At the beginning of the analysis, the visited states are
represented by the empty set. At various steps in the
analysis, we add a tuple to the set. If the tuple already
existed in the set, the fixed point calculation would
immediately terminate the current branch of execution.

After passing the first control state, the set of
reached states is \\
$\{(1, \{x_0 \in P, x_1 \in P, x_2 \in P\},$ \\
$\{x_0 = 1, x_1 = 2, x_2 = 3\})\}$.

After the next control state, the tuple \\
$(2, \{a \in P, x_0 \in P, x_1 \in P, x_2 \in P\}, \{a = 2, x_0 = 1, x_1 = 2, x_2 = 3\})$ \\
is added to the set of visited states.

The next tuple added is \\
$(3,\{b \in N \cup Z \cup P, a \in P, x_0 \in P, x_1 \in P, x_2 \in P\}, \{a = 2, x_0 = 1, x_1 = 2, x_2 = 3\})$ \\
and next is \\
$(4, \{c \in P, b \in N \cup Z \cup P, a \in P, x_0 \in P, x_1 \in P, x_2 \in P\}, \{c = 2, a = 2, x_0 = 1, x_1 = 2, x_2 = 3\})$.

The conditional goto statements lead to two different
control states each, so our analysis must follow two
distinct branches. The order in which these branches are
analyzed is unimportant, as the execution of one cannot
affect the results of another. In this example, we
analyze the true branch first. The next triple added to
the set of visited states is \\
$(7, \{c \in P, b \in N \cup Z \cup P, a \in P, x_0 \in P, x_1 \in P, x_2 \in P\}, \{b < 0, c = 2, a = 2, x_0 = 1, x_1 = 2, x_2 = 3\})$. \\
Notice that an axiom has been added that asserts that $b$
is less than zero. We proceed to a final control state: \\
$(8, \{c \in P, b \in N \cup Z \cup P, a \in P, x_0 \in P, x_1 \in P, x_2 \in P\}, \{b < 0, c = 3, a = 2, x_0 = 1, x_1 = 2, x_2 = 3\})$. \\

At this point, this branch of execution terminates.
Because any return to any previously executed state will
follow a path already taken (and reveal no useful
information), states reached along a terminated branch
remain in the set of reached states indefinitely.

The false branch of line 4 executes, adding the following
tuple to the set: \\
$(5, \{c \in P, b \in N \cup Z \cup P, a \in P, x_0 \in P, x_1 \in P, x_2 \in P\}, \{b \ge 0, c = 2, a = 2, x_0 = 1, x_1 = 2, x_2 = 3\})$.

At line 5, we have another branch. As before, we choose
the true branch for convenience: \\
$(7, \{c \in P, b \in N \cup Z \cup P, a \in P, x_0 \in P, x_1 \in P, x_2 \in P\}, \{b > 2, b \ge 0, c = 2, a = 2, x_0 = 1, x_1 = 2, x_2 = 3\})$
and then
$(8, \{c \in P, b \in N \cup Z \cup P, a \in P, x_0 \in P, x_1 \in P, x_2 \in P\}, \{b > 2, b \ge 0, c = 3, a = 2, x_0 = 1, x_1 = 2, x_2 = 3\})$.

This branch of analysis also terminates, as it has reached its
final control state. We proceed to the final remaining branch
of termination:
$(6, \{c \in P, b \in N \cup Z \cup P, a \in P, x_0 \in P, x_1 \in P, x_2 \in P\}, \{b < 2, b \ge 0, c = 2, a = 2, x_0 = 1, x_1 = 2, x_2 = 3\})$.

The next step in the analysis must ensure that $x[b]$ is a valid
array reference. The assertion that $b \ge 3$ is inconsistent
with the previously existing set of axioms (really, with one
of the previously existing axioms: $b < 2$), so the SAT solver
must say that no satisfying assignment is possible. Similarly,
the assertion that $b < 0$ is inconsistent with the previously
existing axiom that $b \ge 0$. We conclude that the array
access must be safe and continue.

We continue:
$(7, \{c \in P, b \in N \cup Z \cup P, a \in N \cup Z \cup P, x_0 \in P, x_1 \in P, x_2 \in P\}, \{b < 2, b \ge 0, c = 2, x_0 = 1, x_1 = 2, x_2 = 3\})$.
While it may be possible to specify some aspects of $a$'s value,
our analysis does not attempt such a calculation. $a$ is now
undefined.

With
$(8, \{c \in P, b \in N \cup Z \cup P, a \in N \cup Z \cup P, x_0 \in P, x_1 \in P, x_2 \in P\}, \{c = 3, b < 2, b \ge 0, x_0 = 1, x_1 = 2, x_2 = 3\})$,
the last remaining branch of analysis terminates. All array
accesses were proven safe and our analyzer certifies that
Program 1 is safe.

As every tuple generated in this analysis is unique, the
fixed point calculation has no effect on the outcome of the
analysis.

\clearpage
\begin{figure}
\caption{Program 1 Generated Java AST}
\label{fig:p1java}
\begin{verbatim}
import java.util.HashMap;
import controlGraph.*;

public class StatementFactory {
  public static void main(String [] args) {
    // This hash records each label on the first pass.
    HashMap<String, Integer> labels = new HashMap<String, Integer>();
    Statement first = new DeclarationStatement("int", "x", 3, new ArrayLitExpression(
        new Expression[] {new LValueInt(1), new LValueInt(2), new LValueInt(3)}));
    Statement decl14 = new DeclarationStatement("int", "a", 0, new LValueInt(2));
    Statement decl15 = new DeclarationStatement("int", "b", 0,
        UndefinedExpression.getInstance());
    Statement decl16 = new DeclarationStatement("int", "c", 0, new LValueInt(2));
    Statement cond17 = new ConditionalGoto("end",
        new ArithExpr("<", new Variable("b"), new LValueInt(0)));
    Statement cond18 = new ConditionalGoto("end",
        new ArithExpr(">", new Variable("b"), new LValueInt(2)));
    Statement assign19 = new AssignmentStatement(new Variable("a"),
        new ArrayRef(new Expression[] {new Variable("x"), new Variable("b")}));
    labels.put("end", Statement.getLastNum());
    Statement assign20 = new AssignmentStatement(new Variable("c"), new LValueInt(3));

    // Make a fake successor statement
    Statement.doneWithStatements();
    try {
      // Make a second pass, this time through the AST.
      // This gets line numbers from label names.
      Statement.processLabels(labels);

      // Begin the graph search
      first.visitSuccessors(new store(), new ArrayArith());
    } catch(InstantiationException ie) {

      // If a label is referenced, but never defined, we have
      // an invalid program. Print an error and exit.
      System.err.println("Bad label: " + ie.getMessage());
    }
  }
}
\end{verbatim}
\end{figure}
\clearpage

\begin{figure}
\caption{Program 1 Output}
\label{p1output}
Safe
\end{figure}


\begin{figure}
\caption{Program 2 C Code}
\label{p2code}
\begin{verbatim}
     int x[3] = {1,2,3};
     int a = 2;
     int b;
     int c = 2;
     if (b<0) goto end;
     if (b>x[a]) goto end;
     a = x[b];
end: c = 3;
\end{verbatim}
\end{figure}


\begin{figure}
\caption{Program 2 Output}
\label{p2output}
Unsafe. ArrayOverBoundAccess at b in x
\end{figure}

\begin{figure}
\caption{Program 3 C Code}
\label{p3code}
\begin{verbatim}
     int x[3] = {1,2,3};
     int a = 2;
     int b;
     int c = 2;
     int y;
     if (b<0) goto end;
     if (y>=x[a]) goto end;
     if (b>y) goto end;
     a = x[b];
end: c = 3;
\end{verbatim}
\end{figure}

\begin{figure}
\caption{Program 3 Output}
\label{p3output}
Safe
\end{figure}

\newpage
\subsection{Summary}

Examples 1 and 3 are determined to be safe,
whereas the example 2 is not: in program 2, \texttt{b} might
have the value \texttt{3}. In this case, the access to
\texttt{x} just before the end of the program would be
out-of-bounds.

\newpage \section{Division of Labor} Petey and Balaji both took
active part in the design of the array bound verifier.

Petey wrote the lexer, parser, and translator. He also designed
the general structure of the code and started each of the
Statement Java classes. Included in this was a first draft of
the actual abstract interpretation.

Balaji completed the Statement classes and did most of the work
on the Expression Java classes. He also implemented most of the
final version of the abstract interpretation implementation.

Petey wrote the introduction and most of the discussion section.
He also did most of the formatting work and some of the results
section.

Balaji did some of the discussion section and most of the
results section.

%\clearpage

\begin{thebibliography}{4}

\bibitem{tour} Seeley, D.: A Tour of the Worm,
\url{http://www.thehackademy.net/madchat/vxdevl/avtech/A\%20Tour\%20of\%20the\%20Worm.pdf}

\end{thebibliography}

\end{document}


